/* HEADER FILE FOR PUBCRAWL PROBLEM */

#include "params.h"

#define debug (true)

#define smartDelegate (false)
#define smartGuard (false)
#define accumulativeCounting (false)

#define isSmartDelegate (!intoxicated[myID] && smartDelegate)
#define isDumbDelegate (!intoxicated[myID] && !smartDelegate)
#define isSmartGuard (intoxicated[myID] && smartGuard)
#define isDumbGuard (intoxicated[myID] && !smartGuard)

#define isWenchA (inVote.country == wenchA.country && inVote.guard == wenchA.guard)
#define isWenchB (inVote.country == wenchB.country && inVote.guard == wenchB.guard)

#define normalNomination (wenchA.country == 0 && wenchA.guard == 1 && wenchB.country == 0 && wenchB.guard == 0)
#define expectedVote (inVote.country == outVote.country && inVote.guard == outVote.guard)

/* --------------- NUMERIC CONSTANTS ---------------- */
mtype = { ack , dwench, gwench , drink, serving}

/* ------------- DATA TYPES -------------------------*/
typedef person {
	byte country;
	bool guard;
};

/* ----------- MESSAGE CHANNELS ----------------*/

/* Main channel used between delegate bodyguard pairs */
chan channel[N] = [N] of {byte, person, byte};
chan drinkChannel[N] = [N] of {byte, mtype};
/* Driver channel used for designated driver to control
		the flow of the pubcrawl simulation */
chan driverChannel = [N] of {byte, mtype};

/* -------------- GLOBAL VARIABLES ------------*/

/* "Invisible" to delegates */
byte pubList[N];
bool intoxicated[N];
byte currentPub[N];

/* "Visisble" to delegates */
byte pubA, pubB;
byte pubsVisited;
person wenchA, wenchB;
bool barrier1, barrier2, barrier3, barrier4, barrier5;
bool guardIntoxicated;
bool terminate;

/* --------------- INLINE FUNCTIONS -----------*/

inline COINFLIP(vote) {
	atomic {
		if
			:: vote = pubA;
			:: vote = pubB;
		fi
	}
}

inline SHUFFLE_LIST() {
	atomic {
		byte n = 0;
		byte i = 0;
		byte j = N/2;
		byte temp;
		do
			:: i = (i+1)%N;
			:: j = (j+1)%N;
			:: temp = pubList[i];
					pubList[i] = pubList[j];
					pubList[j] = temp;
					n++;
			:: (n>10) -> break;
		od
	}
}

inline CHOOSE_TWO() {
	atomic {
		byte i;
		if
			:: pubA == 255 ->
				for (i : 0 .. (N-1)) {
					if
						:: pubList[i] != 255 ->
							pubA = pubList[i];
							pubList[i] = 255;
							break;
						:: else -> skip
					fi
				}
			:: else -> skip
		fi;
	
		if
		 :: pubB == 255 ->
			for (i : 0 .. (N-1)) {
				if
					:: pubList[i] != 255 ->
						pubB = pubList[i];
						pubList[i] = 255;
						break;
					:: else -> skip
				fi
			}
			:: else -> skip
		fi;
	
		if
			:: (pubA == 255 && pubB != 255) -> pubA = pubB
			:: (pubA != 255 && pubB == 255) -> pubB = pubA
			:: else -> skip
		fi;	
	}
}

inline CHECK_PUB_WIN(cont, correctPub) {
	atomic {
		correctPub = 255;
		cont = true;
		if
			:: debug -> printf ("Checking win condition after pub vote\n")
			:: else -> skip
		fi;

		for(K : 0 .. (N-1)) {
			if
				:: debug && intoxicated[K] -> printf ("Delegate %d is intoxicated\n", K);
				:: debug && !intoxicated[K] -> printf ("Delegate %d is at pub %d\n", K, currentPub[K]);
				:: else -> skip;
			fi;
			
			if 
				:: intoxicated[K] -> skip;
				:: else ->
					if 
						:: (correctPub == 255) -> correctPub = currentPub[K]
						:: (correctPub == currentPub[K]) -> skip
						:: else -> cont = false	
					fi
			fi
							
		}
	}
}